double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
↳ QTRS
↳ Overlay + Local Confluence
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
DOUBLE(s(x)) → DOUBLE(x)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
DOUBLELIST(cons(x, xs)) → DOUBLE(x)
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
DOUBLELIST(cons(x, xs)) → DEL(first(cons(x, xs)), cons(x, xs))
DOUBLELIST(cons(x, xs)) → FIRST(cons(x, xs))
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
DOUBLE(s(x)) → DOUBLE(x)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
DOUBLELIST(cons(x, xs)) → DOUBLE(x)
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
DOUBLELIST(cons(x, xs)) → DEL(first(cons(x, xs)), cons(x, xs))
DOUBLELIST(cons(x, xs)) → FIRST(cons(x, xs))
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
IF(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
IF(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
IF(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
DOUBLE(s(x)) → DOUBLE(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
double(0) → 0
double(s(x)) → s(s(double(x)))
del(x, nil) → nil
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
first(nil) → 0
first(cons(x, xs)) → x
doublelist(nil) → nil
doublelist(cons(x, xs)) → cons(double(x), doublelist(del(first(cons(x, xs)), cons(x, xs))))
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
double(0)
double(s(x0))
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
doublelist(nil)
doublelist(cons(x0, x1))
double(0)
double(s(x0))
doublelist(nil)
doublelist(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
DOUBLELIST(cons(x, xs)) → DOUBLELIST(del(first(cons(x, xs)), cons(x, xs)))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(first(cons(x, xs)), x), first(cons(x, xs)), x, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(first(cons(x, xs)), x), first(cons(x, xs)), x, xs))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), first(cons(x, xs)), x, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), first(cons(x, xs)), x, xs))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
first(cons(x, xs)) → x
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, nil) → nil
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
eq(0, 0) → true
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
del(x, nil) → nil
eq(0, s(y)) → false
eq(s(x), 0) → false
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
first(nil)
first(cons(x0, x1))
first(nil)
first(cons(x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
DOUBLELIST(cons(x, xs)) → DOUBLELIST(if(eq(x, x), x, x, xs))
eq(0, 0) → true
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
del(x, nil) → nil
eq(0, s(y)) → false
eq(s(x), 0) → false
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
POL(0) = 0
POL(DOUBLELIST(x1)) = x1
POL(cons(x1, x2)) = 1 + x2
POL(del(x1, x2)) = x2
POL(eq(x1, x2)) = 0
POL(false) = 0
POL(if(x1, x2, x3, x4)) = 1 + x4
POL(nil) = 0
POL(s(x1)) = 0
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ PisEmptyProof
↳ QTRS
eq(0, 0) → true
eq(s(x), s(y)) → eq(x, y)
if(true, x, y, xs) → xs
if(false, x, y, xs) → cons(y, del(x, xs))
del(x, cons(y, xs)) → if(eq(x, y), x, y, xs)
del(x, nil) → nil
eq(0, s(y)) → false
eq(s(x), 0) → false
del(x0, nil)
del(x0, cons(x1, x2))
if(true, x0, x1, x2)
if(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
nil > false > true > eq2
nil > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
0 > false > true > eq2
0 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
s1 > eq2
equalbool2 > eq2
or2 > eq2
not1 > false > true > eq2
not1 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
isatrue1 > false > true > eq2
isatrue1 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
isafalse1 > false > true > eq2
isafalse1 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
equalsort[a4]2 > false > true > eq2
equalsort[a4]2 > false > [if4, del2] > [cons2, and2] > [if'4, del'2] > eq2
equalsort[a19]2 > eq2
equalsort[a37]2 > true > eq2
witnesssort[a37] > eq2
if4: [4,2,3,1]
eq2: multiset
if'4: [4,2,3,1]
equalsort[a19]2: multiset
true: multiset
or2: multiset
and2: [2,1]
0: multiset
del2: [2,1]
del'2: [2,1]
equalbool2: multiset
cons2: [2,1]
not1: [1]
equalsort[a4]2: multiset
witnesssort[a37]: multiset
isafalse1: multiset
false: multiset
s1: multiset
equalsort[a37]2: multiset
nil: multiset
isatrue1: [1]
if'(true, x11, y9, xs4) → true
if'(false, x18, y15, xs8) → del'(x18, xs8)
del'(x25, cons(y21, xs12)) → if'(eq(x25, y21), x25, y21, xs12)
del'(x32, nil) → false
eq(0, 0) → true
eq(s(x4), s(y3)) → eq(x4, y3)
if(true, x11, y9, xs4) → xs4
if(false, x18, y15, xs8) → cons(y15, del(x18, xs8))
del(x25, cons(y21, xs12)) → if(eq(x25, y21), x25, y21, xs12)
del(x32, nil) → nil
eq(0, s(y32)) → false
eq(s(x45), 0) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a4](nil, nil) → true
equal_sort[a4](nil, cons(x0, x1)) → false
equal_sort[a4](cons(x0, x1), nil) → false
equal_sort[a4](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a4](x0, x2), equal_sort[a4](x1, x3))
equal_sort[a19](0, 0) → true
equal_sort[a19](0, s(x0)) → false
equal_sort[a19](s(x0), 0) → false
equal_sort[a19](s(x0), s(x1)) → equal_sort[a19](x0, x1)
equal_sort[a37](witness_sort[a37], witness_sort[a37]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof